import atom.UnaryAtom;
import formula.BinaryFormula;
import formula.UnaryFormula;
import literal.UnaryLiteral;
import proof.ConclusionProof;
import proof.Proof;
import sign.FormulaSign;

import java.util.ArrayList;
import java.util.Random;

public class GF5 {

    public ArrayList<String> getElement(){
        String[] alphabet={"a","b","c","d","e","f","g","h","i","j","k","l","m","n",
                "o","p","q","r","s","t","u","v","w","x","y","z"};
        ArrayList<String> arr=new ArrayList<>();
        for (int i = 0; i < 5; i++) {//在alphabet中挑选5个字母作为初始输入
            Random random=new Random();
            int randomInt=random.nextInt(26);
            String atom=alphabet[randomInt];
            arr.add(atom);
        }
//        for (String str:arr) {
//            System.out.println(str);
//        }
        return arr;
    }

    public BinaryFormula generateBF(ArrayList<String> arr){
        UnaryFormula uf1=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(0)),false));
        UnaryFormula uf2=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(1)),false));
        UnaryFormula uf3=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(2)),false));
        UnaryFormula uf4=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(3)),false));
        UnaryFormula uf5=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(4)),false));
        ArrayList<UnaryFormula> ufArr=new ArrayList<>();
        ufArr.add(uf1);
        ufArr.add(uf2);
        ufArr.add(uf3);
        ufArr.add(uf4);
        ufArr.add(uf5);


        Random random=new Random();
        int e1= random.nextInt(5);
        int e2= random.nextInt(5);//同12行选中的初始字母数量
        Random randomS=new Random();
        int sign=randomS.nextInt(2);//random sign
        if (sign==0){//exist
            //System.out.println("exist");
            BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,ufArr.get(e1),ufArr.get(e2));
            return bf;
        }else{//any
            //System.out.println("any");
            BinaryFormula bf=new BinaryFormula(FormulaSign.ANY,ufArr.get(e1),ufArr.get(e2));
            return bf;
        }
    }

    public BinaryFormula generateTF(ArrayList<String> arr){
        UnaryFormula uf1=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(0)),false));
        UnaryFormula uf2=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(1)),false));
        UnaryFormula uf3=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(2)),false));
        UnaryFormula uf4=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(3)),false));
        UnaryFormula uf5=new UnaryFormula(new UnaryLiteral(new UnaryAtom(arr.get(4)),false));
        ArrayList<UnaryFormula> ufArr=new ArrayList<>();
        ufArr.add(uf1);
        ufArr.add(uf2);
        ufArr.add(uf3);
        ufArr.add(uf4);
        ufArr.add(uf5);

        Random random=new Random();
        int e1= random.nextInt(5);
        int e2= random.nextInt(5);//同12行选中的初始字母数量
        int e3=random.nextInt(5);
        Random randomS=new Random();
        int sign=randomS.nextInt(2);//random sign
        Random randomS2=new Random();
        int sign2=randomS2.nextInt(2);//random sign(inner one)

        if (sign==0){//outer sign is exist
            if (sign2==0){//inner sign is exist
                //total formula is (E,E)
                BinaryFormula bfInner=new BinaryFormula(FormulaSign.EXIST,ufArr.get(e2),ufArr.get(e3));
                BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,ufArr.get(e1),bfInner);
                return bf;
            }else{//inner sign is for any
                //total formula is (E,A)
                BinaryFormula bfInner=new BinaryFormula(FormulaSign.ANY,ufArr.get(e2),ufArr.get(e3));
                BinaryFormula bf=new BinaryFormula(FormulaSign.EXIST,ufArr.get(e1),bfInner);
                return bf;
            }
        }else {//outer sign is for all
            if (sign2==0){//inner sign is exist
                //total formula is (A,E)
                BinaryFormula bfInner=new BinaryFormula(FormulaSign.EXIST,ufArr.get(e2),ufArr.get(e3));
                BinaryFormula bf=new BinaryFormula(FormulaSign.ANY,ufArr.get(e1),bfInner);
                return bf;
            }else{//inner sign is for any
                //total formula is (A,A)
                BinaryFormula bfInner=new BinaryFormula(FormulaSign.ANY,ufArr.get(e2),ufArr.get(e3));
                BinaryFormula bf=new BinaryFormula(FormulaSign.ANY,ufArr.get(e1),bfInner);
                return bf;
            }
        }
    }

    public BinaryFormula generateConclusion(ArrayList<String> arr){
        Random random=new Random();
        int flag= random.nextInt(2);
        if (flag==0){//生成bf
            return generateBF(arr);
        }else {//生成tf
            return generateTF(arr);
        }
    }

    public ArrayList<Proof> typeChange(ArrayList<BinaryFormula> conditions){
        //接收formula，转换成proof
        ArrayList<Proof> proofs=new ArrayList<>();
        Proof p1=new ConclusionProof(conditions.get(0));
        Proof p2=new ConclusionProof(conditions.get(1));
        Proof p3=new ConclusionProof(conditions.get(2));
        Proof p4=new ConclusionProof(conditions.get(3));
        Proof p5=new ConclusionProof(conditions.get(4));
        proofs.add(p1);
        proofs.add(p2);
        proofs.add(p3);
        proofs.add(p4);
        proofs.add(p5);

        return proofs;

    }

    public boolean show(ArrayList<Proof> proofs,BinaryFormula conclusion){
        if (Solve.solveHelper(proofs,conclusion, new UsedCondition())!=null){
//            System.out.println("conditions:");
//            for (Proof proof:proofs) {
//                System.out.println(proof);
//            }
//            System.out.println("  ");
//            System.out.println("conclusion:");
//            System.out.println(conclusion);
//            System.out.println("  ");
//            System.out.println(Solve.solveHelper(proofs,conclusion, new UsedCondition()));
//            System.out.println("  ");
            return true;
        }else {
            return false;
        }
    }

    public ArrayList<BinaryFormula> bf5(ArrayList<String> arr){//生成5个bf
        ArrayList<BinaryFormula> bfs=new ArrayList<>();
        for (int i = 0; i < 5; i++) {
            BinaryFormula bf=generateBF(arr);
            bfs.add(bf);
        }
        return bfs;
    }

    public ArrayList<BinaryFormula> bf1(ArrayList<String> arr){//1 bf+4 tf
        ArrayList<BinaryFormula> bfs=new ArrayList<>();
        BinaryFormula bf=generateBF(arr);
        bfs.add(bf);//1 bf
        for (int i = 0; i < 4; i++) {//4 tf
            BinaryFormula tf=generateTF(arr);
            bfs.add(tf);
        }
        return bfs;
    }

    public ArrayList<BinaryFormula> bf2(ArrayList<String> arr){//2 bf+3 tf
        ArrayList<BinaryFormula> bfs=new ArrayList<>();
        for (int i=0;i<2;i++){//2 bf
            BinaryFormula bf=generateBF(arr);
            bfs.add(bf);
        }

        for (int i = 0; i < 3; i++) {//3 tf
            BinaryFormula tf=generateTF(arr);
            bfs.add(tf);
        }
        return bfs;
    }

    public ArrayList<BinaryFormula> bf3(ArrayList<String> arr){//3 bf+2 tf
        ArrayList<BinaryFormula> bfs=new ArrayList<>();
        for (int i=0;i<3;i++){//3 bf
            BinaryFormula bf=generateBF(arr);
            bfs.add(bf);
        }

        for (int i = 0; i < 2; i++) {//2 tf
            BinaryFormula tf=generateTF(arr);
            bfs.add(tf);
        }
        return bfs;
    }

    public ArrayList<BinaryFormula> bf4(ArrayList<String> arr){//4 bf+1 tf
        ArrayList<BinaryFormula> bfs=new ArrayList<>();
        for (int i=0;i<4;i++){//4 bf
            BinaryFormula bf=generateBF(arr);
            bfs.add(bf);
        }

        for (int i = 0; i < 1; i++) {//1 tf
            BinaryFormula tf=generateTF(arr);
            bfs.add(tf);
        }
        return bfs;
    }

    public ArrayList<BinaryFormula> bf0(ArrayList<String> arr){//0 bf+5 tf
        ArrayList<BinaryFormula> tfs=new ArrayList<>();
        for (int i = 0; i < 5; i++) {//5 tf
            BinaryFormula tf=generateTF(arr);
            tfs.add(tf);
        }
        return tfs;
    }

    public boolean run(int input){
        ArrayList<String> arr=getElement();
        BinaryFormula conclusion=generateConclusion(arr);
        if (input==5){//bf5
            ArrayList<BinaryFormula> conditions=bf5(arr);
            ArrayList<Proof> proofs=typeChange(conditions);
            boolean flag=show(proofs,conclusion);
            if (flag){
                return true;
            }else {return false;}
        }
        else if (input==1){//bf1+tf4
            ArrayList<BinaryFormula> conditions=bf1(arr);
            ArrayList<Proof> proofs=typeChange(conditions);
            boolean flag=show(proofs,conclusion);
            if (flag){
                return true;
            }else {return false;}
        }
        else if (input==2){//bf2+tf3
            ArrayList<BinaryFormula> conditions=bf2(arr);
            ArrayList<Proof> proofs=typeChange(conditions);
            boolean flag=show(proofs,conclusion);
            if (flag){
                return true;
            }else {return false;}
        }
        else if (input==3){//bf3+tf2
            ArrayList<BinaryFormula> conditions=bf3(arr);
            ArrayList<Proof> proofs=typeChange(conditions);
            boolean flag=show(proofs,conclusion);
            if (flag){
                return true;
            }else {return false;}
        }
        else if (input==4){//bf4+tf1
            ArrayList<BinaryFormula> conditions=bf4(arr);
            ArrayList<Proof> proofs=typeChange(conditions);
            boolean flag=show(proofs,conclusion);
            if (flag){
                return true;
            }else {return false;}
        }
        else if (input==0){//bf0+tf5
            ArrayList<BinaryFormula> conditions=bf0(arr);
            ArrayList<Proof> proofs=typeChange(conditions);
            boolean flag=show(proofs,conclusion);
            if (flag){
                return true;
            }else {return false;}
        }else {
            return false;
        }
    }


    public static void main(String[] args) {
        GF5 gf=new GF5();
        float count=0;
        for (int i=0;i<1000;i++){
            if (gf.run(5)){
                count=count+1;
            }
        }
        System.out.println("done");
        System.out.println(count);
        float probability=(count/1000)*100;//概率的百分比
        String formatted = String.format("%.2f", probability);
        //System.out.println(probability);
        System.out.println("P="+formatted+"%");
    }
}
